Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    perfectp(0)  → false
2:    perfectp(s(x))  → f(x,s(0),s(x),s(x))
3:    f(0,y,0,u)  → true
4:    f(0,y,s(z),u)  → false
5:    f(s(x),0,z,u)  → f(x,u,minus(z,s(x)),u)
6:    f(s(x),s(y),z,u)  → if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
There are 4 dependency pairs:
7:    PERFECTP(s(x))  → F(x,s(0),s(x),s(x))
8:    F(s(x),0,z,u)  → F(x,u,minus(z,s(x)),u)
9:    F(s(x),s(y),z,u)  → F(s(x),minus(y,x),z,u)
10:    F(s(x),s(y),z,u)  → F(x,u,z,u)
The approximated dependency graph contains one SCC: {8,10}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.03 seconds)   ---  May 4, 2006